Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(f(X)) → c(f(g(f(X))))
c(X) → d(X)
h(X) → c(d(X))

The replacement map contains the following entries:

f: {1}
c: empty set
g: empty set
d: empty set
h: {1}


↳ CSR
  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(f(X)) → c(f(g(f(X))))
c(X) → d(X)
h(X) → c(d(X))

The replacement map contains the following entries:

f: {1}
c: empty set
g: empty set
d: empty set
h: {1}

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, h, F, H} are replacing on all positions.
The symbols in {c, g, d, C, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

F(f(X)) → C(f(g(f(X))))
H(X) → C(d(X))


The hidden terms of R are:

f(g(f(X)))
f(X)

Every hiding context is built from:

f on positions {1}

Hence, the new unhiding pairs DPu are :

U(f(x_0)) → U(x_0)
U(f(g(f(X)))) → F(g(f(X)))
U(f(X)) → F(X)

The TRS R consists of the following rules:

f(f(X)) → c(f(g(f(X))))
c(X) → d(X)
h(X) → c(d(X))

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 3 less nodes.
The rules U(f(g(f(z0)))) → F(g(f(z0))) and F(f(x0)) → C(f(g(f(x0)))) form no chain, because ECapµ(F(g(f(z0)))) = F(g(f(z0))) does not unify with F(f(x0)). 

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, h} are replacing on all positions.
The symbols in {c, g, d, U} are not replacing on any position.

The TRS P consists of the following rules:

U(f(x_0)) → U(x_0)

The TRS R consists of the following rules:

f(f(X)) → c(f(g(f(X))))
c(X) → d(X)
h(X) → c(d(X))

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(f(x_0)) → U(x_0)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSDPSubtermProof
            ↳ QCSDP
              ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, h} are replacing on all positions.
The symbols in {c, g, d} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

f(f(X)) → c(f(g(f(X))))
c(X) → d(X)
h(X) → c(d(X))

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.